k:, f:(k). size(k;f)  (k+1) 

latex

Definitions	size(k;f), i=j, , t  T, x:AB(x), {i..j}, , x:A. B(x), {x:A| B(x) }, P  Q, ij, False, A, AB, #$n, -n, n+m, n-m, a<b, Void, x:AB(x), P & Q, i  j < k, , s = t, Type, b, b, Prop, if b t else f fi, f(a), P  Q, Unit, left+right, S  T, S  T
Lemmas	ifthenelse wf, eq int wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, le wf, int seg wf, bool wf, ge wf, nat properties, nat wf